COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.require "memo.pub[let,jmc]" source
C00009 ENDMK
C⊗;
.require "memo.pub[let,jmc]" source;
.FONT A "MATH55";
.turn on "α";
.cb TRULY INVARIANT ASSERTIONS


	This is a variant of the invariant assertion method for proving
programs correct.  The idea is to use assertions that are true at all
program points and whose truth is preserved by the execution of all
statements.  The existence of such %2truly invariant assertions%1
(abbreviated TIA) may depend on the presence of additional %2ghost
variables%1 in the program.  The main utility of the TIA method is
expected to be for proving correctness of programs with concurrent
processes, because it can help avoid considering n-tuplets of program
points.

	We shall proceed by discussing two examples.  The
first is a program discussed by Susan Owicki at the WG2.2
meeting in Tampere, Finland, August 1976.  Owicki's program
is

.begin nofill
.turn on "∂";
%2
.skip 2
∂(24)s ← 0
.skip 1
∂(24)%3cobegin%2
.skip 3
∂(8)s ← s + f(x)∂(32)s ← s + g(x)
.skip 3
∂(24)%3coend%1
.skip 3
.end
%1
	The object is to prove that when the program terminates,
we have %2s = f(x) + g(x)%1, regardless of the order in which the
parallel operations are carried out, but with the obvious
condition that each assignment statement is carried out without
interference.  In order to get suitable TIAs, we add Boolean
ghost variables ⊗p and ⊗q, so that the program becomes

.begin nofill
.turn on "∂";
%2
.skip 2
∂(24)s ← 0
∂(24)p ← q ← %3false%2
.skip 1
∂(24)%3cobegin%2
.skip 3
∂(8)s ← s + f(x)∂(32)s ← s + g(x)
∂(8)p ← %3true%2∂(32)q ← %3false%2
.skip 3
∂(24)%3coend%1
.skip 2
.end
%1
%1
	We assume that each boxed set of statements is carried out
unitarily.  The %2truly invariant assertion%1 is

	%2(¬p ∧ ¬q ∧ s=0) ∨ (p ∧ ¬q ∧ s=f(x)) ∨ (¬p ∧ q ∧ s=g(x)) ∨ (p ∧ q ∧ s=f(x)+g(x))%1,

taking into account each pair of program points.  However,
it can also be written more elegantly as

	%2s = (%3if %2p %3then %2f(x)%3 else %20) + (%3if %2q %3then %2g(x) %3 else %20)%1.

Either form of the assertion is true at all pairs of program points.

	We give a second more elaborate example:
.begin nofill; narrow 0,0;indent 0,0,0;
.at 8 ⊂if filling then break else "        " ⊃;

%3begin
	integer %2n, s; %3processor array %2proc[1:500];

%3boolean array %2q[1:500], r[1:500];

	s ← 0; n ← 0;

%3for %2i ← 1:500 %3do begin %2q[i] ← r[i] ← %3false end%2;

	%3for%2 i ← 1:500%3 do start %2proc[i];

	%3if%2 super(i) %3then

		begin

			for %2j ← 1:500 %3do if%2 j≠i %3then kill%2 proc[j];

			s ← 1000;  q[i] ← %3true%2;

			%3go to%2 done;

		%3end%2;

	%3if %2good(i) %3then %2s ← s + 1;

	%3protect begin

		%2n ← n + 1;

		%3if %2n < 500 %3then kill %2proc[i]; r[i] ← %3true%2

	%3end

end%2;

done:
.end
%1
	The idea of this program is that it sets up 500 processes each
of which tests an ⊗i between 1 and 500.  If a process finds an ⊗i 
satisfying ⊗super(i), it sets ⊗s to 1000, stops all the other
processes and goes to ⊗done.  If ⊗i statisfies ⊗good(i), then it
adds 1 to the count ⊗s, and commits suicide if it isn't the last
processor to finish.  The Boolean variables ⊗q[1:500] and ⊗r[1:500] 
are ghost variables used only in writing the TIA.  I don't especially
advocate the notation used for parallel processing.  It is ad hoc
for the example.  It may need to be said that each process starts
at the statement following the statement that creates them.

	The TIA is
.skip 1
	%2s = %3if %2(∃k.q[k] ∧ super(k)) %3then %21000
%3else %Aα$%2(%3if %2r[k] ∧ good(k) %3then %21 %3else %20)%1.
.skip 1
It is easily verified that this assertion is true at all n-tuplets
of program points, making suitable assumptions about the completion
of statements without interference.

	Perhaps the idea can also be applied to intermittent assertions.
.skip 2
.begin verbatim
John McCarthy
Computer Science Department
Stanford University
Stanford, CA 94305
.end